Added enum types and verification by cheestree · Pull Request #168 · liquid-java/liquidjava

cheestree · 2026-03-03T18:20:23Z

Closes #23. This pull request introduces support for Java enums in the refinement type system and SMT translation. The changes include updates to the grammar, AST, visitors, and Z3 translation logic, as well as new test cases for correct and incorrect enum usages.

An enumerate rule and ENUM token for expressions like Color.Red and the respective AST node to represent enum literals.
The ExpressionVisitor was updated to handle and map enum literals with Z3's enum sorts and constants, while the translator creates and caches these.
The MethodsFirstChecker and RefinementTypeChecker have also been modified to add into the global context instead of just local and to recognize field accesses and annotate them with the proper refinement metadata for type checking

A set of tests was added to verify the valid/invalid behaviour of enum refinements, both Refinement and StateRefinement.

Added a test for enums to, in the future, help clean the refinement message.

rcosta358

Nice work! Left some feedback about the parsing, representation, scoping and translation of enums.
Additionally, we need more tests to verify the correctness of this implementation.

rcosta358 · 2026-03-04T14:35:16Z

liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4

 	ID_UPPER '(' args? ')';

+enumCall: 
+	OBJECT_TYPE;


I understand you used OBJECT_TYPE because of the rule ambiguity. However, this raises a concern, because it allows for multiple chaining of ids (e.g., Mode.photo.photo, Mode.photo.photo.photo, etc.) which should not be syntactically valid.

We could avoid the ambiguity by forcing the OBJECT_TYPE to always start with a lowercase letter and declare enumCall as ID '.' ID, but Java packages are allowed start with an uppercase letter (even though it's highly discouraged).

So, we can introduce another terminal, just for enums:

enumCall: ENUM_CALL; // ... ENUM_CALL: [a-zA-Z_][a-zA-Z0-9_]* '.' [a-zA-Z_][a-zA-Z0-9_]*;

This way, you guarantee the enums are always represented by two ids separated by a dot, without ambiguity.

That's understandable, my issue with that, at the time of development, was if ID and ID_UPPER wouldn't, even if they are slightly different, lead to ambiguity due to other grammar rules. I should've explored more formats.

It would be nice to have support for enums that live in another package, via qualified name. I agree with @rcosta358 that we want a first version working, and then we can think about this. To achieve this, we need a name resolution (à lá Spoon).

rcosta358 · 2026-03-04T14:38:24Z

liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java

+    private String enumCreate(EnumContext rc) {
+        String enumText = rc.enumCall().getText();
+        int lastDot = enumText.lastIndexOf('.');
+        String enumClass = enumText.substring(0, lastDot);
+        String enumConst = enumText.substring(lastDot + 1);
+        String varName = String.format(Formats.ENUM_VALUE, enumClass, enumConst);
+        return varName;


I don't like the "enum#%s#%s" format because it's hard to read in the error messages. Here you can simply return the enumText, and everywhere else still use this format but change it to "%s.%s" instead.

I should've gone with a better format, I admit. I wasn't sure due to the rest of the existing types.

We might want to "decode" enums when they come back in the error messages back to their Refinement version. Two approaches: 1) having a translation map. 2) storing the source of each variable in the Verification Condition (I'm doing this in aeon, and I think we discussed it for LJ).

This is not specific for Enums, we might want to do this for other types.

liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java

rcosta358 · 2026-03-04T14:54:00Z

...java-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java

+            String varName = String.format(Formats.ENUM_VALUE, enumName, ev.getSimpleName());
+            Predicate refinement = Predicate.createEquals(Predicate.createVar(varName),
+                    Predicate.createLit(String.valueOf(ordinal), Types.INT));
+            context.addGlobalVariableToContext(varName, qualifiedEnumName, enumRead.getReference(), refinement);


Why global? Shouldn't it only be visible within the class or package where it was declared?

If there is an enum that is used across methods, and a shared package is needed, when the context is reinitialized, the local context is cleaned. If it's kept in the global context, the placement is irrelevant.
For example, the following common package a layer above the testSuite.

When line 134 is changed to context.addVarToContext(varName, enumRead.getReference(), refinement, enumRead), the following occurs:

That's not really a shared package because it's not even included in the verification, each test is ran individually from its file or folder.

The issue is: if I declare an enum X in class A, should I be able to use it in class B? It might be fine, just raising some questions about how it should work.

Also, if we can use enums from different classes, we should make sure they have their fully qualified name to distinguish enums with the same name from different classes.

I didn't realize the testing was that restrictive. I can try and create some test scenarios that take into consideration global and local context. The other option would be to restrict enum verification to only in the same file, but that feels like a cop-out instead of an actual fix/intended functionality. 🤔

liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java

liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java

...java-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java

Created AST node and visitors for enums. Changed grammar as suggested to specific rules and positioning to avoid ambiguity. Changed format.

cheestree · 2026-03-04T19:53:27Z

The change to using EnumSort seems to have worked, but I'm still unsure of how exactly tests for this should be created if some problematic areas are based off of package/class location. Is there a currently implemented test that runs off of its own folder and has multiple components in different files?

rcosta358 · 2026-03-04T20:00:07Z

Currently every test file/folder is verified completely isolated from one another. Everything needed for it should be in the corresponding file/folder, even if that means unwanted repetition.

Fixed grammar so that it required uppercase start for both parts. Differentiates between types and calls.

This reverts commit c831921.

This reverts commit d785934.

Translation is now done in 2 phases: a first one for enums, and storing their constant values and names, and the second one as previously done, but with special attention now due to the presence of enums. If the variable, when translating, is already present, it isn't added, and there are no duplicates.

cheestree · 2026-03-05T22:36:40Z

This seems to be the best outcome for now, as enums aren't duplicated if present via checking using a map. It looks like a O(n^2) situation but since there aren't usually a lot of enum values for a single type, it is (in my opinion) negligible.

Added 2 error tests for enum: when setting null on a field with an enum refinement, and on a function parameter refinement. A successful error test was added as well to test backtracking to a null state.

rcosta358

Left some minor comments.

liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java

liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enumerate.java

Added some more enum tests for different situations (like as parameters or fields with enum refinements). Merged CorrectEnumResetMode into CorrectEnumUsage (redundant having a separate one that only tests resetting to null) Refactored enumCreate as suggested. Refactored grammar to follow Enumerate class.

Moved and refactored the RefinmentMessage test to be a very simple Refinement checker.

cheestree added 2 commits March 3, 2026 00:45

Added enum type support with tests

a08dbad

Added EnumRefinementMessage test

3835584

Added a test for enums to, in the future, help clean the refinement message.

rcosta358 requested changes Mar 4, 2026

View reviewed changes

rcosta358 assigned cheestree Mar 4, 2026

rcosta358 added the enhancement New feature or request label Mar 4, 2026

Applied fixes and suggestions for enums

3d7fb5d

Created AST node and visitors for enums. Changed grammar as suggested to specific rules and positioning to avoid ambiguity. Changed format.

cheestree added 5 commits March 4, 2026 20:07

Fixed grammar

c831921

Fixed grammar so that it required uppercase start for both parts. Differentiates between types and calls.

Revert "Fixed grammar"

d785934

This reverts commit c831921.

Reapply "Fixed grammar"

66e982f

This reverts commit d785934.

Refactored variable translation

9e79999

Added enum tests

cf9e867

Added 2 error tests for enum: when setting null on a field with an enum refinement, and on a function parameter refinement. A successful error test was added as well to test backtracking to a null state.

rcosta358 reviewed Mar 9, 2026

View reviewed changes

cheestree added 4 commits March 11, 2026 12:10

Moved RefinementMessage test

f2b1b7f

Moved and refactored the RefinmentMessage test to be a very simple Refinement checker.

Changed Enumerate to Enum

8f734c2

Renamed fields and getters/setters

64fe267

rcosta358 requested a review from CatarinaGamboa March 11, 2026 16:56

Conversation

cheestree commented Mar 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

rcosta358 left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rcosta358 Mar 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rcosta358 Mar 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rcosta358 Mar 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

cheestree commented Mar 4, 2026

Uh oh!

rcosta358 commented Mar 4, 2026

Uh oh!

cheestree commented Mar 5, 2026

Uh oh!

rcosta358 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

cheestree commented Mar 3, 2026 •

edited

Loading

rcosta358 left a comment •

edited

Loading

rcosta358 Mar 4, 2026 •

edited

Loading

rcosta358 Mar 4, 2026 •

edited

Loading

rcosta358 Mar 4, 2026 •

edited

Loading